0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 7 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 InliningProof (UPPER BOUND(ID), 1006 ms)
↳12 CpxRNTS
↳13 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CpxRNTS
↳15 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 IntTrsBoundProof (UPPER BOUND(ID), 133 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 35 ms)
↳20 CpxRNTS
↳21 ResultPropagationProof (UPPER BOUND(ID), 2 ms)
↳22 CpxRNTS
↳23 IntTrsBoundProof (UPPER BOUND(ID), 387 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 121 ms)
↳26 CpxRNTS
↳27 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳28 CpxRNTS
↳29 IntTrsBoundProof (UPPER BOUND(ID), 167 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 43 ms)
↳32 CpxRNTS
↳33 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳34 CpxRNTS
↳35 IntTrsBoundProof (UPPER BOUND(ID), 228 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 77 ms)
↳38 CpxRNTS
↳39 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳40 CpxRNTS
↳41 IntTrsBoundProof (UPPER BOUND(ID), 206 ms)
↳42 CpxRNTS
↳43 IntTrsBoundProof (UPPER BOUND(ID), 63 ms)
↳44 CpxRNTS
↳45 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳46 CpxRNTS
↳47 IntTrsBoundProof (UPPER BOUND(ID), 1335 ms)
↳48 CpxRNTS
↳49 IntTrsBoundProof (UPPER BOUND(ID), 2465 ms)
↳50 CpxRNTS
↳51 FinalProof (⇔, 0 ms)
↳52 BOUNDS(1, n^1)
f(C(x1, x2)) → C(f(x1), f(x2))
f(Z) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
g(x) → x
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
f(C(x1, x2)) → C(f(x1), f(x2)) [1]
f(Z) → Z [1]
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1]
eqZList(C(x1, x2), Z) → False [1]
eqZList(Z, C(y1, y2)) → False [1]
eqZList(Z, Z) → True [1]
second(C(x1, x2)) → x2 [1]
first(C(x1, x2)) → x1 [1]
g(x) → x [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]
f(C(x1, x2)) → C(f(x1), f(x2)) [1]
f(Z) → Z [1]
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1]
eqZList(C(x1, x2), Z) → False [1]
eqZList(Z, C(y1, y2)) → False [1]
eqZList(Z, Z) → True [1]
second(C(x1, x2)) → x2 [1]
first(C(x1, x2)) → x1 [1]
g(x) → x [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]
f :: C:Z → C:Z C :: C:Z → C:Z → C:Z Z :: C:Z eqZList :: C:Z → C:Z → False:True and :: False:True → False:True → False:True False :: False:True True :: False:True second :: C:Z → C:Z first :: C:Z → C:Z g :: g → g |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
f
second
first
g
eqZList
and
and(v0, v1) → null_and [0]
null_and, const
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Z => 0
False => 1
True => 2
null_and => 0
const => 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(2, 2) :|: z = 1 + 0 + 0, z' = 1 + 0 + 0
eqZList(z, z') -{ 3 }→ and(2, 1) :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0
eqZList(z, z') -{ 3 }→ and(2, 1) :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 3 }→ and(1, 2) :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, 2) :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0
eqZList(z, z') -{ 3 }→ and(1, 1) :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ x :|: x >= 0, z = x
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ x :|: x >= 0, z = x
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
{ g } { and } { first } { f } { second } { eqZList } |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: ?, size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: ?, size: O(1) [2] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: ?, size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: ?, size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] second: runtime: ?, size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] eqZList: runtime: ?, size: O(1) [2] |
and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), and(eqZList(x11, y11), eqZList(x21, y21))) :|: x1' >= 0, x2' >= 0, y2' >= 0, y21 >= 0, y11 >= 0, x11 >= 0, x21 >= 0, z = 1 + (1 + x1' + x2') + (1 + x11 + x21), y1' >= 0, z' = 1 + (1 + y1' + y2') + (1 + y11 + y21)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 2) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: x1' >= 0, x2' >= 0, y2' >= 0, z' = 1 + (1 + y1' + y2') + 0, x12 >= 0, x22 >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + (1 + x12 + x22)
eqZList(z, z') -{ 3 }→ and(and(eqZList(x1', y1'), eqZList(x2', y2')), 1) :|: y22 >= 0, x1' >= 0, x2' >= 0, y12 >= 0, y2' >= 0, y1' >= 0, z = 1 + (1 + x1' + x2') + 0, z' = 1 + (1 + y1' + y2') + (1 + y12 + y22)
eqZList(z, z') -{ 3 }→ and(2, and(eqZList(x17, y17), eqZList(x27, y27))) :|: x27 >= 0, x17 >= 0, y27 >= 0, z = 1 + 0 + (1 + x17 + x27), y17 >= 0, z' = 1 + 0 + (1 + y17 + y27)
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x13, y13), eqZList(x23, y23))) :|: x23 >= 0, x13 >= 0, z' = 1 + 0 + (1 + y13 + y23), x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x13 + x23), y13 >= 0, y23 >= 0, x2'' >= 0
eqZList(z, z') -{ 3 }→ and(1, and(eqZList(x15, y15), eqZList(x25, y25))) :|: z = 1 + 0 + (1 + x15 + x25), z' = 1 + (1 + y1'' + y2'') + (1 + y15 + y25), y2'' >= 0, x25 >= 0, y1'' >= 0, y25 >= 0, x15 >= 0, y15 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 3 }→ 2 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, 2 = 2
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 1 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, 2 = 2, 1 = 1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + (1 + x14 + x24), x14 >= 0, x24 >= 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, y24 >= 0, z' = 1 + 0 + (1 + y14 + y24), x2'' >= 0, y14 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z' = 1 + 0 + 0, x1'' >= 0, z = 1 + (1 + x1'' + x2'') + 0, x2'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x16 + x26), y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, x26 >= 0, x16 >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: y26 >= 0, z = 1 + 0 + 0, y16 >= 0, z' = 1 + (1 + y1'' + y2'') + (1 + y16 + y26), y2'' >= 0, y1'' >= 0, v0 >= 0, v1 >= 0, 1 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, y2'' >= 0, y1'' >= 0, z' = 1 + (1 + y1'' + y2'') + 0, v0 >= 0, v1 >= 0, 1 = v0, 2 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + (1 + x18 + x28), z' = 1 + 0 + 0, x28 >= 0, x18 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + (1 + y18 + y28), y18 >= 0, y28 >= 0, v0 >= 0, v1 >= 0, 2 = v0, 1 = v1
eqZList(z, z') -{ 3 }→ 0 :|: z = 1 + 0 + 0, z' = 1 + 0 + 0, v0 >= 0, v1 >= 0, 2 = v0, 2 = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 3 + 2·x1 + 2·x2 }→ 1 + s + s' :|: s >= 0, s <= 1 * x1, s' >= 0, s' <= 1 * x2, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g(z) -{ 1 }→ z :|: z >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
g: runtime: O(1) [1], size: O(n1) [z] and: runtime: O(1) [0], size: O(1) [2] first: runtime: O(1) [1], size: O(n1) [z] f: runtime: O(n1) [1 + 2·z], size: O(n1) [z] second: runtime: O(1) [1], size: O(n1) [z] eqZList: runtime: O(n1) [78 + 156·z'], size: O(1) [2] |